Stéphane Graham-Lengrand

Non-idempotent intersection types and quantitative information about reduction paths: a survey

Over the recent years, a new area in the study of intersection types has been explored. In the original spirit of intersection types, a term is of type A /\ B if it is both of type A and of type B, which naturally leads to an idempotent view of intersections: A /\ A is the same type as A. Dropping this idempotency property of intersections allows the design of resource-aware type systems, with deep connections to linear logic. This enriches typing with quantitative information about the lengths of reduction paths from typed terms. Upper bounds for these lengths -or even sometimes exact characterisations- have been provided by such typing systems, for various abstract machines and reduction strategies in the lambda-calculus and some of its variants. Among these, explicit substitution calculi proved a particularly appropriate approach to establishing such results. We will review this line of research, where typing is brought much closer to operational and denotational semantics